Cannot set OPTIONS pragmas --allow-unsolved-metas
--no-positivity-check --no-termination-check --type-in-type
--injective-type-constructors --experimental-irrelevance
with safe flag.
